[WangPD94] Wang Yi, Paul Pettersson and Mats Daniels.Automatic Verification of Real-Time Communicating Systems by Constraint Solving. In Proceedings of the 7th International Conference on Formal Description Techniques, pages 223-238, North-Holland. 1994.

[Mat09] The MathWorks. Stateflow and Stateflow Coder User's Guide, March 2009.

[SCAIFESCTM04] N. Scaife, C. Sofronis, P. Caspi, S. Tripakis, and F. Maraninchi, Defining and translating a safe- subset of Simulink/Stateflow into Lustre, EMSOFT 2004 ACM, pp. 259-268.

[HAMON&RUSHBY07] G. Hamon and J. M. Rushby, An operational semantics for Stateflow, International Journal on Software Tools for Technology Transfer, 9(5-6): 447-456, 2007.

[UMLGuide] G. Booch, J. Rumbaugh and I. Jacobson, The Unified Modeling Language User Guide SECOND EDITION, Addison Wesley Professional, 2005.

[HOARE85] C.A. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, New Jersey, 1985.

[GAMMAHJV95]E. Gamma, R. Helm, R. E. Johnson, and J. Vlissides. DesignPatterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995.

[HUTH&Ryan04]. Micheal Huth and Mark Ryan. Logic in Computer Science. ?SPAN class=GramE>Cambridge University Press 2004.

[ROSCOE97] A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.

[LIUSD08b] Y. Liu, J. Sun and J. S. Dong: An Analyzer for Extended Compositional Process Algebras. ICSE Companion 2008: 919-920. Bib

[AWR97] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.

[GJH97] G. J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5):279?95, 1997.

[SUNLDP09] J. Sun, Y. Liu, J. S. Dong and J. Pang: Towards Flexible Verification under Fairness. CAV 2009.

[LIUSD10] Yang Liu, Jun Sun and Jin Song Dong: Analyzing Hierarchical Complex Real-time Systems. FSE 2010.

[LIUPSZ09] Y. Liu, J. Pang, J. Sun and J. H. Zhao. Verification of Population Ring Protocols in PAT. TASE 2009.

[SUNLDC09] J. Sun, Y. Liu, J. S. Dong and C. Q. Chen. Integrating Specification and Programs for System Modeling and Verification. TASE 2009.

[ZHANGLSDCL09] S. J. Zhang, Y. Liu, J. Sun, J. S. Dong, W. Chen and Y. A. Liu. Formal Verification of Scalable NonZero Indicators. SEKE 2009.

[LIUWLS09]  Y. Liu, W. Chen, Y. A. Liu and J. Sun. Model Checking Linearizability via Refinement. FM 09.

[SUNLRLD09]  J. Sun, Y. Liu, A. Roychoudhury, S. S. Liu and J. S. Dong. Fair Model Checking with Process Counter Abstraction. FM 09.

[SUNLDZ09]  J. Sun, Y. Liu, J. S. Dong and X. Zhang. Verifying Stateful Timed CSP using Implicit Clocks and Zone Abstraction. ICFEM 09.

[LIUSD09] Y. Liu,  J. Sun and J. S. Dong. Scalable Multi-Core Model Checking Fairness Enhanced Systems. ICFEM 09.

[ZHAO10] W. Zhao. Yet Another Model Checker for PROMELA - theTransformation Approach. In MoCSeRS 2010, pages 131?32. IEEE Computer Society, 2010.

[ZHANGL10] S. Zhang and Y. Liu. An Automatic Approach to Model Checking UML State Machines. In SSIRI 2010, pages 131?32. IEEE Computer Society, 2010.

[ORCUserGuide] http://orc.csres.utexas.edu/userguide/pdf/all.pdf.

[AQDKJM09] A. Q. David Kitchin and J. Misra. Quicksort: Combining concurrency, recursion, and mutable data structures. Technical report, The University of Texas at Austin, Department of Computer Sciences."

[MAJM10] M. AlTurki and J. Meseguer. Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis. Technical report, https://www.ideals.illinois.edu/handle/2142/15414.